
\begin{figure*}[htpb!]
\begin{center}
\begin{tabular}{|l|l|}
\hline

$\code{FT} ::= \hC\hgn{\code{FO},\code{IP}}$ & Field (and method return) Type. \\

$\code{T} ::= \hC\hgn{\code{MO},\code{IP}}$ & Type. \\

$\code{N} ::= \hC\hgn{\code{NO},\code{NI}}$ & Non-variable type (for objects). \\

$\code{NO} ::= \World ~|~ \colorbox{light}{\hl}$ & Non-variable Owner parameter (for objects). \\

$\code{FO} ::= \code{NO} ~|~ \This ~|~ \hO$ & Field Owner parameter. \\

$\code{MO} ::= \code{FO} ~|~ \code{?}$ & Method Owner parameter (including generic wildcard). \\

$\code{NI} ::= \Mutable ~|~ \colorbox{light}{$\Immut_\hl$}$ & Non-variable Immutability parameter (for objects). \\

$\code{VI} ::= \code{NI} ~|~ \Immut ~|~ \hI$ & Variable Immutability for \code{new}. \\

$\code{IP} ::= \ReadOnly ~|~ \code{VI}$ & Immutability Parameter. \\

$\code{IG} ::= \ReadOnly ~|~ \Immut ~|~ \Mutable ~|~ \Raw$ & Immutability method Guard. \\

$\hM ::= \code{<I extends IG>?} ~ \code{FT} ~ \hm\hparen{\ol{\code{T}} ~ \ol{\hx}} ~ \lb\ \hreturn ~ \he\texttt{;}~\rb$
& Method declaration. \\

$\hL ::= \hclass ~ \hC\hgn{\hO,\hI}\code{~extends~C'}\hgn{\hO,\hI} \lb\ \ol{\code{FT}}~\ol{\hf}\texttt{;} \ol{\hM}~\rb$
& cLass declaration. \\

%\code{~K~}
%$\hK ::= \code{C}\hparen{\ol{\hT} ~ \ol{\hx}} ~ \lb\ \code{super}\hparen{\ol{\hf}}\texttt{;}\code{~this.}\ol{\hf}\code{~=~}\ol{\hf}\texttt{;~}\he\texttt{;~} \rb$
%& Constructor declaration. \\

$\hv ::= \code{null} ~|~ \colorbox{light}{\hl} $
& Values: either \code{null} or a location~\hl. \\


% No cast: \hparen{\hT} ~ \he ~|~
$\he ::= \hv ~|~ \hx ~|~ \he.\hf ~|~ \he.\hf = \he ~|~ \he.\hm\hparen{\ol{\he}} ~|~ \hnew ~ \hC\hgn{\code{FO},\code{VI}}\hparen{\ol{\he}}  ~|~ \colorbox{light}{\he\code{;return l}}$
& Expressions. \\ %: values, parameters, field access\&assignment, invocation, \code{new} start\&finish

\hline
\end{tabular}
\end{center}
\caption{FOIGJ Syntax. The terminals are \code{null},
    owner parameters~(\hO, \This, \World),
    and immutability parameters~(\hI, \ReadOnly, \Mutable, \Raw, \Immut).
    Given a location~\hl, $\Immut_\hl$ represents an immutable object with cooker~\hl.
    The program source code cannot contain the grayed elements (locations are only created during execution/reduction in \RULE{R-New} of \Ref{Figure}{reduction}).
    }
\label{Figure:syntax}
\end{figure*}
